(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun al (Int) Bool)
(declare-fun m (Int) Bool)
(declare-fun ap (Int) Bool)
(declare-fun ar (Int) Bool)
(declare-fun e (Int) Int)
(declare-fun n (Int) Int)
(declare-fun f (Int) Bool)
(declare-fun o (Int) Bool)
(declare-fun ab (Int) Bool)
(declare-fun a (Int) Bool)
(assert (let ((a (o 1))(am (n 2))) (let ((g (<= 1 am))) (= g a))))
(assert (let ((an (e 0))(cd 0)(h 0)(i (f 0))) (let ((j (ite i cd an))(ao (a (- 1)))) (let ((k (ite ao j h))(l (= b 0))) (let ((p (ite l 0 k))(d 0)) (= d p))))))
(assert (let ((cg c)(ax (+ c (- 1)))) (let ((ba ax)) (let ((bb (+ 1 ba))(bc (a c))) (let ((bd (ite bc bb ba))(be (ar c))) (let ((bf (ite be bd ba))(bg (ab c))) (let ((bh (ite bg 1 ba))(bi (ap c))) (let ((bj (ite bi bh bf))(bk 0)(aw (o c))) (let ((bl (ite aw bk ba))(bm (m c))) (let ((bn (ite bm bl bj))(bo (f c))) (let ((ch (ite bo b ba))(bp (al c))) (let ((bq (ite bp ch bn))(br (= c b))) (let ((bs (ite br 0 bq))) (= bs cg))))))))))))))
(check-sat)
